1. $T$ : Type
\\[0ex]$\vdash$  $\forall$$x$:$T$, $L$:($T$ List). ($x$ $\in$ nth\_tl(0;$L$)) $\Rightarrow$ ($x$ $\in$ $L$)